Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		times(x,plus(y,1))	→ plus(times(x,plus(y,times(1,0))),x)
2:		times(x,1)	→ x
3:		plus(x,0)	→ x
4:		times(x,0)	→ 0

There are 4 dependency pairs:


5:		TIMES(x,plus(y,1))	→ PLUS(times(x,plus(y,times(1,0))),x)
6:		TIMES(x,plus(y,1))	→ TIMES(x,plus(y,times(1,0)))
7:		TIMES(x,plus(y,1))	→ PLUS(y,times(1,0))
8:		TIMES(x,plus(y,1))	→ TIMES(1,0)

The approximated dependency graph contains one SCC: {6}.

Consider the SCC {6}. The constraints could not be solved.

Tyrolean Termination Tool (0.09 seconds) --- May 4, 2006